R:Realizer. ((Rplus?(R)))  ((Rnone?(R)))  ([[R]] ~ @R-loc(R): R-base-ma(R)) 

latex

Definitions

SQType(T), , case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), True, if b then t else f fi , tt, ff, x. t(x), t  T, [[R]], Rnone?(x1), Rplus?(x1), b, P  Q, x:A. B(x), {T}, False, x(s), Unit, A, Realizer, left  right, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(),

Lemmas

es realizer wf, msystem wf, false wf, true wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf